\begin{tabbing}
ES\{i\}
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$E$:Type$_{\mbox{\scriptsize i}}$\+
\\[0ex]$\times$EqDecider($E$)
\\[0ex]$\times$${\it pred?}$:($E$$\rightarrow$($E$+Unit))
\\[0ex]$\times$${\it info}$:($E$$\rightarrow$(Id$\times$Id+(IdLnk$\times$$E$)$\times$Id))
\\[0ex]$\times$EO\=rderAxioms\{i\}($E$;\+
\\[0ex]${\it pred?}$;
\\[0ex]${\it info}$)
\-\\[0ex]$\times$$T$:(Id$\rightarrow$Id$\rightarrow$Type$_{\mbox{\scriptsize i}}$)
\\[0ex]$\times$$V$:(Id$\rightarrow$Id$\rightarrow$Type$_{\mbox{\scriptsize i}}$)
\\[0ex]$\times$$M$:(IdLnk$\rightarrow$Id$\rightarrow$Type$_{\mbox{\scriptsize i}}$)
\\[0ex]$\times$${\it init}$:($i$:Id$\rightarrow$$x$:Id$\rightarrow$$T$($i$,$x$))
\\[0ex]$\times$${\it Trans}$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$($x$:Id$\rightarrow$\=$T$\+
\\[0ex]($i$
\\[0ex],$x$)))
\-\\[0ex]$\times$${\it val}$:($e$:$E$$\rightarrow$kindcase(kind(${\it info}$;$e$); $a$.$V$(loc(${\it info}$;$e$),$a$); $l$,$t$.$M$($l$,$t$) ))
\\[0ex]$\times$${\it Send}$:(\=$i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$\+
\\[0ex](Msg($M$) List))
\-\\[0ex]$\times$${\it Choose}$:($i$:Id$\rightarrow$$a$:Id$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$($V$($i$,$a$)+Unit))
\\[0ex]$\times$val{-}axiom(\=$E$;$V$;$M$;${\it info}$;${\it pred?}$;\+
\\[0ex]${\it init}$;${\it Trans}$;${\it Choose}$;
\\[0ex]${\it Send}$;${\it val}$)
\-\\[0ex]$\times$(\=($\forall$$i$:Id, $x$:Id. AtomFree(Type$_{\mbox{\scriptsize i}}$;$T$($i$,$x$)))\+
\\[0ex]\& ($\forall$$i$:Id, $a$:Id. AtomFree(Type$_{\mbox{\scriptsize i}}$;$V$($i$,$a$)))
\\[0ex]\& ($\forall$$l$:IdLnk, ${\it tg}$:Id. AtomFree(Type$_{\mbox{\scriptsize i}}$;$M$($l$,${\it tg}$))))
\-\\[0ex]$\times$Top
\-
\end{tabbing}